Over the past two decades several fragments of first-order logic have beenidentified and shown to have good computational and algorithmic properties, toa great extent as a result of appropriately describing the image of thestandard translation of modal logic to first-order logic. This applies mostnotably to the guarded fragment, where quantifiers are appropriatelyrelativized by atoms, and the fragment defined by restricting the number ofvariables to two. The aim of this talk is to review recent work concerningthese fragments and their popular extensions. When presenting the materialspecial attention is given to decision procedures for the finite satisfiabilityproblems, as many of the fragments discussed contain infinity axioms. Wehighlight most effective techniques used in this context, their advantages andlimitations. We also mention a few open directions of study.
展开▼
